package org.eclipse.iota.util;

import java.util.ArrayList;
import java.util.HashSet;
import java.util.List;
import java.util.Set;

import org.eclipse.iota.IotaPackage;
import org.eclipse.iota.assignments.Assignment;
import org.eclipse.iota.assignments.SubstitutionAssignmentGenerator;
import org.eclipse.iota.model.Clause;
import org.eclipse.iota.model.Constraint;
import org.eclipse.iota.model.Equation;
import org.eclipse.iota.model.Existential;
import org.eclipse.iota.model.Expression;
import org.eclipse.iota.model.Reference;
import org.eclipse.iota.model.Variable;

/**
 * Utility methods for variables.
 * @author Christian Krause
 * @generated NOT
 */
public class IotaVariableUtil {
	
	/**
	 * Get a list of all variables that are declared for
	 * the argument clause. Make sure that the clause is contained
	 * in a predicate!
	 * @param clause Clause.
	 * @return Variables.
	 */
	public static List<Variable> getVariables(Clause clause) {
		List<Variable> result = new ArrayList<Variable>();
		if (clause.getAlternation()!=null &&
			clause.getAlternation().getDefinition()!=null) {
			result.addAll(clause.getAlternation().getDefinition().getParameters());
		}
		result.addAll(clause.getExistentials());
		return result;
	}
	
	/**
	 * Get a list of used variables in an expression.
	 * @param expression Expression.
	 * @return Variables.
	 */
	public static List<Variable> getUsedVariables(Expression expression) {
		List<Variable> result = new ArrayList<Variable>();
		for (Reference ref : getAllReferences(expression)) {
			if (!result.contains(ref.getVariable())) {
				result.add(ref.getVariable());
			}
		}
		return result;
	}
	
	/**
	 * Get a list of used variables in an equation.
	 * @param equation equation.
	 * @return Variables.
	 */
	public static List<Variable> getUsedVariables(Equation equation) {
		List<Variable> result = new ArrayList<Variable>();
		result.addAll(getUsedVariables(equation.getLeft()));
		result.addAll(getUsedVariables(equation.getRight()));
		return result;
	}

	/**
	 * Gather a list of references contained in an expression.
	 * @param expression Expression.
	 * @return All references.
	 */
	public static List<Reference> getAllReferences(Expression expression) {
		return IotaFindUtil.getAllExpressions(expression, IotaPackage.eINSTANCE.getReference());
	}
	
	/**
	 * Find a variable that satisfies some given constraints. 
	 * @param clause Clause to be searched in.
	 * @param variable The variable that acts as a template / place-holder in the constraint.
	 * @param constraints The constraints that should be satisfied.
	 * @return The variable, if found.
	 */
	public static Variable findSuchThat(Clause clause, Variable variable, Constraint... constraints) {
		
		SubstitutionAssignmentGenerator generator = new SubstitutionAssignmentGenerator();
		
		// Set source and target variables.
		generator.getSources().add(variable);		
		generator.getTargets().addAll(getVariables(clause));
		
		// Source constraints.
		for (Constraint constraint : constraints) {
			generator.getSourceConstraints().add(constraint);
		}
		
		// Target constraints.
		generator.getTargetConstraints().addAll(clause.getConstraints());
		
		// Compute the assignments.
		List<Assignment> assigments = generator.calculateAssigments();
		if (!assigments.isEmpty()) {
			return ((Reference) assigments.get(0).get(variable)).getVariable();
		}
		
		// Not found.
		return null;
		
	}

	/**
	 * Create a fresh existential. This does not add it to the clause.
	 * The method makes sure that there is no existing variable with the same name.
	 * @param clause Clause.
	 * @return Created variable.
	 */
	public static Existential freshExistential(Clause clause) {
		
		// Gather set of existing variable names.
		Set<String> variables = new HashSet<String>();
		for (Variable var : IotaVariableUtil.getVariables(clause)) {
			variables.add(var.getName());
		}
		
		// Create a fresh variable.
		return new Existential(freshVariableName(variables));
	}

	/**
	 * Create a fresh (unused) variable name.
	 * @param variables Existing variables.
	 * @return Fresh name.
	 */
	public static String freshVariableName(Set<String> variables) {
		char ch = 'a';
		String name;		
		while (ch!='z' && variables.contains(name = String.valueOf(ch))) {
			ch++;
		}
		if (variables.contains(name = String.valueOf(ch))) {
			int i = 1;
			while (variables.contains(name = "a"+i)) i++;
		}
		return name;
	}

}
